x:Id, t, v:Top, x1:Id, t1, v1:Top.
x = x1  (x : t initially x = v ||+ x1 : t1 initially x1 = v1) 

latex

Definitions

x:A. B(x), P  Q, A ||+ B, x : t initially x = v, P & Q, M1 || M2, ma-frame-compatible(A;B), mk-ma, x : v, , M1 ||decl M2, f || g, 1of(t), 2of(t), Prop, b, x  dom(f), f(x), deq-member(eq;x;L), reduce(f;k;as), false, Y, if b t else f fi, P  Q, P  Q, t  T, P  Q, ma-frame-compat(A;B), xdom(f). v=f(x)   P(x;v), M.rframe(A.pre p for a), M.frame(k affects x), M.aframe(k affects x), M.rframe(A.effect f of k on y), M.sframe(k sends <l,tg>), M.bframe(k sends on l), M.rframe(A.sends tfL of k on l), z != f(x)  P(a;z), A, False, A & B

Lemmas

and functionality wrt iff, assert wf, assert of bor, false wf, or functionality wrt iff, deq property, bor wf, eqof wf, id-deq wf, bfalse wf, Knd wf, IdLnk wf, not wf, Id wf, top wf